normal{-}ds\{i:l\}(${\it ds}$) $\,\equiv$$_{\mbox{\scriptsize def}}$$\;\;$fpf{-}all(Id; IdDeq; ${\it ds}$; $x$,$A$.normal{-}type\{i:l\}($A$))